Inference at * 2 1 1 1 
Iof proof for Lemma member nth tl:

.....assertion..... NILNIL

1. T : Type
2. n : 
3. 0 < n
4. x:T, L:(T List). (x  nth_tl(n - 1;L))  (x  L)
5. T
6. T List
  n:. nth_tl(n;[]) = [] 

latex

 by ((InductionOnNat) 
CollapseTHEN (((Reduce 0) 
CollapseTHEN (Auto)))) 

latex

C1: .....upcase..... NILNIL

C1: 7. n1 : 
C1: 8. 0 < n1
C1: 9. nth_tl(n1 - 1;[]) = []
C1:   nth_tl(n1;[]) = []
C.

Definitions	Void, n+m, -n, A, False, P  Q, i  j , A  B, t  T, {x:A| B(x)} , , i z j, i <z j, nth_tl(n;as), n - m, #$n, [], x:A. B(x), x:AB(x), a < b, , Type, s = t, type List
Lemmas	ge wf, nat properties, nat wf, nat ind tp